YES 1.53
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((elem :: Eq a => [a] -> [[a]] -> Bool) :: Eq a => [a] -> [[a]] -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((elem :: Eq a => [a] -> [[a]] -> Bool) :: Eq a => [a] -> [[a]] -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (elem :: Eq a => [a] -> [[a]] -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2600), Succ(xv4000000)) → new_primPlusNat(xv2600, xv4000000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2600), Succ(xv4000000)) → new_primPlusNat(xv2600, xv4000000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30000), Succ(xv400000)) → new_primMulNat(xv30000, Succ(xv400000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30000), Succ(xv400000)) → new_primMulNat(xv30000, Succ(xv400000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(ty_[], bcd)) → new_esEs0(xv302, xv4002, bcd)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, ba), bb), bc) → new_esEs(xv300, xv4000, ba, bb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bd), bc) → new_esEs0(xv300, xv4000, bd)
new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(app(app(ty_@3, hb), hc), hd))) → new_esEs3(xv300, xv4000, hb, hc, hd)
new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(app(ty_Either, gh), ha))) → new_esEs2(xv300, xv4000, gh, ha)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(ty_@2, bcb), bcc)) → new_esEs(xv302, xv4002, bcb, bcc)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, bac), bad), hg, hh) → new_esEs2(xv300, xv4000, bac, bad)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(app(ty_Either, bbe), bbf)), hh)) → new_esEs2(xv301, xv4001, bbe, bbf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(ty_Maybe, bce)) → new_esEs1(xv302, xv4002, bce)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], baa)), hg), hh)) → new_esEs0(xv300, xv4000, baa)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(ty_[], bcd))) → new_esEs0(xv302, xv4002, bcd)
new_esEs2(Left(xv300), Left(xv4000), app(app(ty_Either, ff), fg), fb) → new_esEs2(xv300, xv4000, ff, fg)
new_esEs2(Left(xv300), Left(xv4000), app(app(app(ty_@3, fh), ga), gb), fb) → new_esEs3(xv300, xv4000, fh, ga, gb)
new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, dg), dh))) → new_esEs(xv300, xv4000, dg, dh)
new_esEs2(Left(xv300), Left(xv4000), app(ty_Maybe, fd), fb) → new_esEs1(xv300, xv4000, fd)
new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(ty_[], gf))) → new_esEs0(xv300, xv4000, gf)
new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xv300, xv4000, ee, ef, eg)
new_esEs1(Just(xv300), Just(xv4000), app(app(ty_Either, ec), ed)) → new_esEs2(xv300, xv4000, ec, ed)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(app(app(ty_@3, bch), bda), bdb))) → new_esEs3(xv302, xv4002, bch, bda, bdb)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, bac), bad)), hg), hh)) → new_esEs2(xv300, xv4000, bac, bad)
new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, fd)), fb)) → new_esEs1(xv300, xv4000, fd)
new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(ty_Maybe, gg))) → new_esEs1(xv300, xv4000, gg)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(app(ty_@3, dc), dd), de)) → new_esEs3(xv301, xv4001, dc, dd, de)
new_esEs2(Right(xv300), Right(xv4000), gc, app(app(ty_@2, gd), ge)) → new_esEs(xv300, xv4000, gd, ge)
new_esEs2(Right(xv300), Right(xv4000), gc, app(app(ty_Either, gh), ha)) → new_esEs2(xv300, xv4000, gh, ha)
new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, ec), ed))) → new_esEs2(xv300, xv4000, ec, ed)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(ty_[], cf)) → new_esEs0(xv301, xv4001, cf)
new_esEs1(Just(xv300), Just(xv4000), app(ty_Maybe, eb)) → new_esEs1(xv300, xv4000, eb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(ty_@2, cd), ce)) → new_esEs(xv301, xv4001, cd, ce)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(ty_Maybe, bce))) → new_esEs1(xv302, xv4002, bce)
new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(app(ty_@2, gd), ge))) → new_esEs(xv300, xv4000, gd, ge)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(ty_[], bbc)), hh)) → new_esEs0(xv301, xv4001, bbc)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bh), ca), cb), bc) → new_esEs3(xv300, xv4000, bh, ca, cb)
new_esEs2(Left(xv300), Left(xv4000), app(ty_[], fc), fb) → new_esEs0(xv300, xv4000, fc)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_Either, bf), bg)), bc)) → new_esEs2(xv300, xv4000, bf, bg)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_[], bd)), bc)) → new_esEs0(xv300, xv4000, bd)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, bae), baf), bag)), hg), hh)) → new_esEs3(xv300, xv4000, bae, baf, bag)
new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], fc)), fb)) → new_esEs0(xv300, xv4000, fc)
new_esEs0(:(xv30, xv31), :(xv400, xv401), bdc) → new_esEs0(xv31, xv401, bdc)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(ty_[], cf))) → new_esEs0(xv301, xv4001, cf)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, bab)), hg), hh)) → new_esEs1(xv300, xv4000, bab)
new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], ea))) → new_esEs0(xv300, xv4000, ea)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(ty_Maybe, bbd)), hh)) → new_esEs1(xv301, xv4001, bbd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs3(xv302, xv4002, bch, bda, bdb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(ty_@2, bba), bbb), hh) → new_esEs(xv301, xv4001, bba, bbb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(ty_[], bbc), hh) → new_esEs0(xv301, xv4001, bbc)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, he), hf), hg, hh) → new_esEs(xv300, xv4000, he, hf)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(app(app(ty_@3, dc), dd), de))) → new_esEs3(xv301, xv4001, dc, dd, de)
new_esEs1(Just(xv300), Just(xv4000), app(app(ty_@2, dg), dh)) → new_esEs(xv300, xv4000, dg, dh)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], baa), hg, hh) → new_esEs0(xv300, xv4000, baa)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(ty_Either, bbe), bbf), hh) → new_esEs2(xv301, xv4001, bbe, bbf)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(ty_Maybe, cg)) → new_esEs1(xv301, xv4001, cg)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(app(ty_@3, bh), ca), cb)), bc)) → new_esEs3(xv300, xv4000, bh, ca, cb)
new_esEs1(Just(xv300), Just(xv4000), app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xv300, xv4000, ee, ef, eg)
new_esEs1(Just(xv300), Just(xv4000), app(ty_[], ea)) → new_esEs0(xv300, xv4000, ea)
new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, fh), ga), gb)), fb)) → new_esEs3(xv300, xv4000, fh, ga, gb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, bab), hg, hh) → new_esEs1(xv300, xv4000, bab)
new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, eh), fa)), fb)) → new_esEs(xv300, xv4000, eh, fa)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_Maybe, be)), bc)) → new_esEs1(xv300, xv4000, be)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(ty_Either, bcf), bcg)) → new_esEs2(xv302, xv4002, bcf, bcg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(app(ty_@3, bbg), bbh), bca), hh) → new_esEs3(xv301, xv4001, bbg, bbh, bca)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(app(ty_@2, bba), bbb)), hh)) → new_esEs(xv301, xv4001, bba, bbb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(ty_Either, da), db)) → new_esEs2(xv301, xv4001, da, db)
new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, ff), fg)), fb)) → new_esEs2(xv300, xv4000, ff, fg)
new_esEs2(Right(xv300), Right(xv4000), gc, app(ty_[], gf)) → new_esEs0(xv300, xv4000, gf)
new_esEs2(Right(xv300), Right(xv4000), gc, app(ty_Maybe, gg)) → new_esEs1(xv300, xv4000, gg)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(app(ty_@2, cd), ce))) → new_esEs(xv301, xv4001, cd, ce)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(app(ty_Either, bcf), bcg))) → new_esEs2(xv302, xv4002, bcf, bcg)
new_esEs2(Left(xv300), Left(xv4000), app(app(ty_@2, eh), fa), fb) → new_esEs(xv300, xv4000, eh, fa)
new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, eb))) → new_esEs1(xv300, xv4000, eb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, bf), bg), bc) → new_esEs2(xv300, xv4000, bf, bg)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(ty_Maybe, cg))) → new_esEs1(xv301, xv4001, cg)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(app(ty_Either, da), db))) → new_esEs2(xv301, xv4001, da, db)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(app(app(ty_@3, bbg), bbh), bca)), hh)) → new_esEs3(xv301, xv4001, bbg, bbh, bca)
new_esEs0(:(xv30, xv31), :(xv400, xv401), app(ty_[], df)) → new_esEs0(xv30, xv400, df)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, he), hf)), hg), hh)) → new_esEs(xv300, xv4000, he, hf)
new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_@2, ba), bb)), bc)) → new_esEs(xv300, xv4000, ba, bb)
new_esEs2(Right(xv300), Right(xv4000), gc, app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(xv300, xv4000, hb, hc, hd)
new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(app(ty_@2, bcb), bcc))) → new_esEs(xv302, xv4002, bcb, bcc)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, bae), baf), bag), hg, hh) → new_esEs3(xv300, xv4000, bae, baf, bag)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, be), bc) → new_esEs1(xv300, xv4000, be)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(ty_Maybe, bbd), hh) → new_esEs1(xv301, xv4001, bbd)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs1(Just(xv300), Just(xv4000), app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xv300, xv4000, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Just(xv300), Just(xv4000), app(app(ty_@2, dg), dh)) → new_esEs(xv300, xv4000, dg, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xv300), Just(xv4000), app(ty_[], ea)) → new_esEs0(xv300, xv4000, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Just(xv300), Just(xv4000), app(app(ty_Either, ec), ed)) → new_esEs2(xv300, xv4000, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Just(xv300), Just(xv4000), app(ty_Maybe, eb)) → new_esEs1(xv300, xv4000, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(app(app(ty_@3, hb), hc), hd))) → new_esEs3(xv300, xv4000, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xv300, xv4000, ee, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(app(app(ty_@3, bch), bda), bdb))) → new_esEs3(xv302, xv4002, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, bae), baf), bag)), hg), hh)) → new_esEs3(xv300, xv4000, bae, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(app(app(ty_@3, dc), dd), de))) → new_esEs3(xv301, xv4001, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(app(ty_@3, bh), ca), cb)), bc)) → new_esEs3(xv300, xv4000, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, fh), ga), gb)), fb)) → new_esEs3(xv300, xv4000, fh, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(app(app(ty_@3, bbg), bbh), bca)), hh)) → new_esEs3(xv301, xv4001, bbg, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, dg), dh))) → new_esEs(xv300, xv4000, dg, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(app(ty_@2, gd), ge))) → new_esEs(xv300, xv4000, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, eh), fa)), fb)) → new_esEs(xv300, xv4000, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(app(ty_@2, bba), bbb)), hh)) → new_esEs(xv301, xv4001, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(app(ty_@2, cd), ce))) → new_esEs(xv301, xv4001, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_@2, ba), bb)), bc)) → new_esEs(xv300, xv4000, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, he), hf)), hg), hh)) → new_esEs(xv300, xv4000, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(app(ty_@2, bcb), bcc))) → new_esEs(xv302, xv4002, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], baa)), hg), hh)) → new_esEs0(xv300, xv4000, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(ty_[], bcd))) → new_esEs0(xv302, xv4002, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(ty_[], gf))) → new_esEs0(xv300, xv4000, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(ty_[], bbc)), hh)) → new_esEs0(xv301, xv4001, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_[], bd)), bc)) → new_esEs0(xv300, xv4000, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], fc)), fb)) → new_esEs0(xv300, xv4000, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xv30, xv31), :(xv400, xv401), bdc) → new_esEs0(xv31, xv401, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(ty_[], cf))) → new_esEs0(xv301, xv4001, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], ea))) → new_esEs0(xv300, xv4000, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xv30, xv31), :(xv400, xv401), app(ty_[], df)) → new_esEs0(xv30, xv400, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(app(ty_Either, gh), ha))) → new_esEs2(xv300, xv4000, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(app(ty_Either, bbe), bbf)), hh)) → new_esEs2(xv301, xv4001, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, bac), bad)), hg), hh)) → new_esEs2(xv300, xv4000, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, ec), ed))) → new_esEs2(xv300, xv4000, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(app(ty_Either, bf), bg)), bc)) → new_esEs2(xv300, xv4000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, ff), fg)), fb)) → new_esEs2(xv300, xv4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(app(ty_Either, bcf), bcg))) → new_esEs2(xv302, xv4002, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(app(ty_Either, da), db))) → new_esEs2(xv301, xv4001, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(Left(xv300), xv31), :(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, fd)), fb)) → new_esEs1(xv300, xv4000, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Right(xv300), xv31), :(Right(xv4000), xv401), app(app(ty_Either, gc), app(ty_Maybe, gg))) → new_esEs1(xv300, xv4000, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), hg), app(ty_Maybe, bce))) → new_esEs1(xv302, xv4002, bce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, bab)), hg), hh)) → new_esEs1(xv300, xv4000, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@3(xv300, xv301, xv302), xv31), :(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, bah), app(ty_Maybe, bbd)), hh)) → new_esEs1(xv301, xv4001, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, app(ty_Maybe, be)), bc)) → new_esEs1(xv300, xv4000, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(Just(xv300), xv31), :(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, eb))) → new_esEs1(xv300, xv4000, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(@2(xv300, xv301), xv31), :(@2(xv4000, xv4001), xv401), app(app(ty_@2, cc), app(ty_Maybe, cg))) → new_esEs1(xv301, xv4001, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(app(ty_@3, dc), dd), de)) → new_esEs3(xv301, xv4001, dc, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bh), ca), cb), bc) → new_esEs3(xv300, xv4000, bh, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs3(xv302, xv4002, bch, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(app(ty_@3, bbg), bbh), bca), hh) → new_esEs3(xv301, xv4001, bbg, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, bae), baf), bag), hg, hh) → new_esEs3(xv300, xv4000, bae, baf, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(xv300), Left(xv4000), app(app(app(ty_@3, fh), ga), gb), fb) → new_esEs3(xv300, xv4000, fh, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xv300), Right(xv4000), gc, app(app(app(ty_@3, hb), hc), hd)) → new_esEs3(xv300, xv4000, hb, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, ba), bb), bc) → new_esEs(xv300, xv4000, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(ty_@2, cd), ce)) → new_esEs(xv301, xv4001, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bd), bc) → new_esEs0(xv300, xv4000, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(ty_[], cf)) → new_esEs0(xv301, xv4001, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(ty_Either, da), db)) → new_esEs2(xv301, xv4001, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, bf), bg), bc) → new_esEs2(xv300, xv4000, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(ty_Maybe, cg)) → new_esEs1(xv301, xv4001, cg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, be), bc) → new_esEs1(xv300, xv4000, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(ty_@2, bcb), bcc)) → new_esEs(xv302, xv4002, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(ty_@2, bba), bbb), hh) → new_esEs(xv301, xv4001, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, he), hf), hg, hh) → new_esEs(xv300, xv4000, he, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv300), Right(xv4000), gc, app(app(ty_@2, gd), ge)) → new_esEs(xv300, xv4000, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(xv300), Left(xv4000), app(app(ty_@2, eh), fa), fb) → new_esEs(xv300, xv4000, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(ty_[], bcd)) → new_esEs0(xv302, xv4002, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(ty_[], bbc), hh) → new_esEs0(xv301, xv4001, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], baa), hg, hh) → new_esEs0(xv300, xv4000, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, bac), bad), hg, hh) → new_esEs2(xv300, xv4000, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(ty_Either, bbe), bbf), hh) → new_esEs2(xv301, xv4001, bbe, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(ty_Either, bcf), bcg)) → new_esEs2(xv302, xv4002, bcf, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(ty_Maybe, bce)) → new_esEs1(xv302, xv4002, bce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, bab), hg, hh) → new_esEs1(xv300, xv4000, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(ty_Maybe, bbd), hh) → new_esEs1(xv301, xv4001, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xv300), Left(xv4000), app(ty_[], fc), fb) → new_esEs0(xv300, xv4000, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv300), Right(xv4000), gc, app(ty_[], gf)) → new_esEs0(xv300, xv4000, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xv300), Left(xv4000), app(app(ty_Either, ff), fg), fb) → new_esEs2(xv300, xv4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv300), Right(xv4000), gc, app(app(ty_Either, gh), ha)) → new_esEs2(xv300, xv4000, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(xv300), Left(xv4000), app(ty_Maybe, fd), fb) → new_esEs1(xv300, xv4000, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv300), Right(xv4000), gc, app(ty_Maybe, gg)) → new_esEs1(xv300, xv4000, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3